{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Application
  ( checkArguments
  , checkArguments_
  , checkApplication
  , inferApplication
  , checkProjAppToKnownPrincipalArg
  , disambiguateConstructor'
  , univChecks
  , suffixToLevel
  ) where

import Prelude hiding ( null )

import Control.Applicative        ( (<|>) )
import Control.Monad.Except       ( ExceptT, runExceptT, MonadError, catchError, throwError )
import Control.Monad.Trans.Maybe

import Data.Bifunctor
import Data.Maybe
import Data.Void
import qualified Data.Foldable as Fold
import qualified Data.IntSet   as IntSet

import Agda.Interaction.Highlighting.Generate
  ( storeDisambiguatedConstructor, storeDisambiguatedProjection )

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern (patternToExpr)
import Agda.Syntax.Abstract.Views as A
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Concrete.Pretty () -- only Pretty instances
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Position

import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.InstanceArguments (postponeInstanceConstraints)
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Modalities
import Agda.TypeChecking.Names
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.Def
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings (warning)

import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List  ( (!!!), initWithDefault )
import qualified Agda.Utils.List as List
import Agda.Utils.List1 ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty ( prettyShow )
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.VarSet as VarSet

import Agda.Utils.Impossible
import Agda.Utils.Singleton (singleton)

---------------------------------------------------------------------------
-- * Data structures for checking arguments
---------------------------------------------------------------------------

-- | Ranges of checked arguments, where present.
type ArgRanges = [Range]

setACElims :: [Elim] -> ArgsCheckState a -> ArgsCheckState a
setACElims es st = st{ acCheckedArgs = go es (acCheckedArgs st) }
  where
    go [] [] = []
    go (e : es) (ca : cas) = ca{ caElim = e } : go es cas
    go _ _ = __IMPOSSIBLE__

-----------------------------------------------------------------------------
-- * Applications
-----------------------------------------------------------------------------

-- | Extract the "head constraints" (currently lock constraints 'CheckLockedVars')
--   from the application checker (final) state.
acHeadConstraints :: (Elims -> Term) -> ArgsCheckState a -> [Constraint]
acHeadConstraints hd = go hd . acCheckedArgs
  where
    go :: (Elims -> Term) -> [CheckedArg] -> [Constraint]
    go hd = \case
      [] -> []
      CheckedArg e _ mc : cas -> applyWhenJust mc (\ c -> (lazyAbsApp c (hd []) :)) $
        go (hd . (e :)) cas

-- | Check the "head constraints" (currently lock constraints 'CheckLockedVars')
--   accumulated during checking of an application.
checkHeadConstraints :: (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints hd st = do
  mapM_ solveConstraint_ $ acHeadConstraints hd st
  return $ hd $ map caElim $ acCheckedArgs st


-- | @checkApplication hd args e t@ checks an application.
--   Precondition: @Application hs args = appView e@
--
--   @checkApplication@ disambiguates constructors
--   (and continues to 'checkConstructorApplication')
--   and resolves pattern synonyms.
checkApplication :: Comparison -> A.Expr -> A.Args -> A.Expr -> Type -> TCM Term
checkApplication cmp hd args e t =
  turnOffExpandLastIfExistingMeta hd $
  postponeInstanceConstraints $ do
  reportSDoc "tc.check.app" 20 $ vcat
    [ "checkApplication"
    , nest 2 $ "hd   = " <+> prettyA hd
    , nest 2 $ "args = " <+> do prettyList $ fmap prettyA args
    , nest 2 $ "e    = " <+> prettyA e
    , nest 2 $ "t    = " <+> prettyTCM t
    ]
  reportSDoc "tc.check.app" 70 $ vcat
    [ "checkApplication (raw)"
    , nest 2 $ text $ "hd   = " ++ show hd
    , nest 2 $ text $ "args = " ++ show (deepUnscope args)
    , nest 2 $ text $ "e    = " ++ show (deepUnscope e)
    , nest 2 $ text $ "t    = " ++ show t
    ]
  case unScope hd of
    -- Subcase: unambiguous projection
    A.Proj o p | Just x <- getUnambiguous p -> do
      checkUnambiguousProjectionApplication cmp e t x o hd args

    -- Subcase: ambiguous projection
    A.Proj o p -> do
      checkProjApp cmp e o (unAmbQ p) hd args t

    -- Subcase: unambiguous constructor
    A.Con ambC | Just c <- getUnambiguous ambC -> do
      -- augment c with record fields, but do not revert to original name
      con <- getOrigConHead c
      checkConstructorApplication cmp e t con hd args

    -- Subcase: ambiguous constructor
    A.Con (AmbQ cs0) -> do
      let cont c = checkConstructorApplication cmp e t c hd args
      afterDisambiguation cont $ disambiguateConstructor cs0 args t

    -- Subcase: pattern synonym
    A.PatternSyn n -> do
      (ns, p) <- lookupPatternSyn n
      p <- return $ setRange (getRange n) $ killRange $ vacuous p   -- Pattern' Void -> Pattern' Expr
      -- Expand the pattern synonym by substituting for
      -- the arguments we have got and lambda-lifting
      -- over the ones we haven't.
      let meta h r = A.Underscore $ A.emptyMetaInfo{ A.metaRange = r, A.metaKind = A.hidingToMetaKind h }   -- TODO: name suggestion
      case A.insertImplicitPatSynArgs meta (getRange n) ns args of
        Nothing      -> typeError $ BadArgumentsToPatternSynonym n
        Just (s, ns) -> do
          let p' = patternToExpr p
              e' = A.lambdaLiftExpr ns (A.substExpr s p')
          checkExpr' cmp e' t

    -- Subcase: macro
    A.Macro x -> do
      -- First go: no parameters
      TelV tel _ <- telView . defType =<< instantiateDef =<< getConstInfo x

      tTerm <- primAgdaTerm
      tName <- primQName

      -- Andreas, 2021-05-13, can we use @initWithDefault __IMPOSSIBLE__@ here?
      let argTel   = init $ telToList tel -- last argument is the hole term

          -- inspect macro type to figure out if arguments need to be wrapped in quote/quoteTerm
          mkArg :: Type -> NamedArg A.Expr -> NamedArg A.Expr
          mkArg t a | unEl t == tTerm =
            (fmap . fmap)
              (A.App (A.defaultAppInfo (getRange a)) (A.QuoteTerm A.exprNoRange) . defaultNamedArg) a
          mkArg t a | unEl t == tName =
            (fmap . fmap)
              (A.App (A.defaultAppInfo (getRange a)) (A.Quote A.exprNoRange) . defaultNamedArg) a
          mkArg t a | otherwise = a

          makeArgs :: [Dom (String, Type)] -> [NamedArg A.Expr] -> ([NamedArg A.Expr], [NamedArg A.Expr])
          makeArgs [] args = ([], args)
          makeArgs _  []   = ([], [])
          makeArgs tel@(d : tel1) (arg : args) =
            case insertImplicit arg tel of
              NoInsertNeeded -> first (mkArg (snd $ unDom d) arg :) $ makeArgs tel1 args
              ImpInsert is   -> makeArgs (drop (length is) tel) (arg : args)
              BadImplicits   -> (arg : args, [])  -- fail later in checkHeadApplication
              NoSuchName{}   -> (arg : args, [])  -- ditto

          (macroArgs, otherArgs) = makeArgs argTel args
          unq = A.App (A.defaultAppInfo $ fuseRange x args) (A.Unquote A.exprNoRange) . defaultNamedArg

          desugared = A.app (unq $ unAppView $ Application (A.Def x) $ macroArgs) otherArgs

      checkExpr' cmp desugared t

    -- Subcase: unquote
    A.Unquote _
      | [arg] <- args -> do
          (_, hole) <- newValueMeta RunMetaOccursCheck CmpLeq t
          unquoteM (namedArg arg) hole t
          return hole
      | arg : args <- args -> do
          -- Example: unquote v a b : A
          --  Create meta H : (x : X) (y : Y x) → Z x y for the hole
          --  Check a : X, b : Y a
          --  Run the tactic on H
          --  Check H a b : A
          tel    <- metaTel args                    -- (x : X) (y : Y x)
          target <- addContext tel newTypeMeta_     -- Z x y
          let holeType = telePi_ tel target         -- (x : X) (y : Y x) → Z x y
          let hd       = namedArg arg
          (Just vs, EmptyTel) <- first allApplyElims <$> checkArguments_ CmpLeq ExpandLast hd args tel
                                                    -- a b : (x : X) (y : Y x)
          (_, hole) <- newValueMeta RunMetaOccursCheck CmpLeq holeType
          unquoteM hd hole holeType
          let rho = reverse (map unArg vs) ++# IdS  -- [x := a, y := b]
          coerce CmpEq (apply hole vs) (applySubst rho target) t -- H a b : A
      where
        metaTel :: [Arg a] -> TCM Telescope
        metaTel []           = pure EmptyTel
        metaTel (arg : args) = do
          a <- newTypeMeta_
          let dom = a <$ domFromArg arg
          ExtendTel dom . Abs "x" <$>
            addContext ("x" :: String, dom) (metaTel args)

    -- Subcase: defined symbol or variable.
    _ -> do
      v <- checkHeadApplication cmp e t hd args
      reportSDoc "tc.term.app" 30 $ vcat
        [ "checkApplication: checkHeadApplication returned"
        , nest 2 $ "v = " <+> prettyTCM v
        ]
      return v

-- | Precondition: @Application hd args = appView e@.
inferApplication :: ExpandHidden -> A.Expr -> A.Args -> A.Expr -> TCM (Term, Type)
inferApplication exh hd args e | not (defOrVar hd) = do
  t <- workOnTypes $ newTypeMeta_
  v <- checkExpr' CmpEq e t
  return (v, t)
inferApplication exh hd args e = postponeInstanceConstraints $ do
  SortKit{..} <- sortKit
  case unScope hd of
    A.Proj o p | isAmbiguous p -> inferProjApp e o (unAmbQ p) hd args
    A.Def' x s | Just (sz, u) <- isNameOfUniv x -> inferUniv sz u e x s args
    _ -> do
      (f, t0) <- inferHead hd
      res <- runExceptT $ checkArgumentsE CmpEq exh hd args t0 Nothing
      case res of
        Right st@(ACState{acType = t1}) -> fmap (,t1) $ unfoldInlined =<< checkHeadConstraints f st
        Left problem -> do
          t <- workOnTypes $ newTypeMeta_
          v <- postponeArgs problem CmpEq exh hd args t0 t $ \ st -> unfoldInlined =<< checkHeadConstraints f st
          return (v, t)

-----------------------------------------------------------------------------
-- * Heads
-----------------------------------------------------------------------------

inferHeadDef :: ProjOrigin -> QName -> TCM (Elims -> Term, Type)
inferHeadDef o x = do
  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
  proj <- isRelevantProjection x
  rel  <- getRelevance . defArgInfo <$> getConstInfo x
  let app =
        case proj of
          Nothing -> \ args -> Def x $ map Apply args
          Just p  -> \ args -> projDropParsApply p o rel args
  first applyE <$> inferDef app x

-- | Infer the type of a head thing (variable, function symbol, or constructor).
--   We return a function that applies the head to arguments.
--   This is because in case of a constructor we want to drop the parameters.
inferHead :: A.Expr -> TCM (Elims -> Term, Type)
inferHead e = do
  case e of
    A.Var x -> do -- traceCall (InferVar x) $ do
      (u, a) <- getVarInfo x
      reportSDoc "tc.term.var" 20 $ hsep
        [ "variable" , prettyTCM x
        , "(" , text (show u) , ")"
        , "has type:" , prettyTCM a
        ]
      unless (usableRelevance a) $
        typeError $ VariableIsIrrelevant x
      -- Andreas, 2019-06-18, LAIM 2019, issue #3855:
      -- Conor McBride style quantity judgement:
      -- The available quantity for variable x must be below
      -- the required quantity to construct the term x.
      -- Note: this whole thing does not work for linearity, where we need some actual arithmetics.
      unlessM ((getQuantity a `moreQuantity`) <$> viewTC eQuantity) $
        typeError $ VariableIsErased x

      unless (usableCohesion a) $
        typeError $ VariableIsOfUnusableCohesion x (getCohesion a)

      unless (usablePolarity a) $
        typeError $ VariableIsOfUnusablePolarity x (getModalPolarity a)

      return (applyE u, unDom a)

    A.Def x  -> inferHeadDef ProjPrefix x
    A.Def'{} -> __IMPOSSIBLE__ -- handled in checkHeadApplication and inferApplication

    A.Proj o ambP | Just d <- getUnambiguous ambP -> inferHeadDef o d
    A.Proj{} -> __IMPOSSIBLE__ -- inferHead will only be called on unambiguous projections

    A.Con ambC | Just c <- getUnambiguous ambC -> do

      -- Constructors are polymorphic internally.
      -- So, when building the constructor term
      -- we should throw away arguments corresponding to parameters.

      -- First, inferDef will try to apply the constructor
      -- to the free parameters of the current context. We ignore that.
      con <- getOrigConHead c
      (u, a) <- inferDef (\ _ -> Con con ConOCon []) c

      -- Next get the number of parameters in the current context.
      Constructor{conPars = n} <- theDef <$> (instantiateDef =<< getConstInfo c)

      reportSLn "tc.term.con" 7 $ unwords [prettyShow c, "has", show n, "parameters."]

      -- So when applying the constructor throw away the parameters.
      return (applyE u . drop n, a)
    A.Con{} -> __IMPOSSIBLE__  -- inferHead will only be called on unambiguous constructors
    A.QuestionMark i ii -> inferMeta i (newQuestionMark ii)
    A.Underscore i      -> inferMeta i (newValueMetaOfKind i RunMetaOccursCheck)
    e -> do
      (term, t) <- inferExpr e
      return (applyE term, t)

inferDef :: (Args -> Term) -> QName -> TCM (Term, Type)
inferDef mkTerm x =
  traceCall (InferDef x) $ do
    -- getConstInfo retrieves the *absolute* (closed) type of x
    -- instantiateDef relativizes it to the current context
    d0 <- getConstInfo x
    d  <- instantiateDef d0
    reportSDoc "tc.term.def" 10 $ "inferDef" <+> prettyTCM x
    reportSDoc "tc.term.def" 30 $ "  absolute type:    " <+> inTopContext (prettyTCM $ defType d0)
    reportSDoc "tc.term.def" 30 $ "  instantiated type:" <+> prettyTCM (defType d)
    -- Irrelevant defs are only allowed in irrelevant position.
    -- Erased defs are only allowed in erased position (see #3855).
    checkModality x d
    reportSDoc "tc.term.def" 30 $ "  checked modality!"
    case theDef d of
      GeneralizableVar{} -> do
        reportSDoc "tc.term.def" 30 $ "  we are a GeneralizableVar"
        -- Generalizable variables corresponds to metas created
        -- at the point where they should be generalized. Module parameters
        -- have already been applied to the meta, so we don't have to do that
        -- here.
        val <- fromMaybe __IMPOSSIBLE__ <$> viewTC (eGeneralizedVars . key x)
        sub <- checkpointSubstitution (genvalCheckpoint val)
        let (v, t) = applySubst sub (genvalTerm val, genvalType val)
        debug [] t v
        return (v, t)
      _ -> do
        reportSDoc "tc.term.def" 30 $ "  we are not a GeneralizableVar"
        -- since x is considered living in the top-level, we have to
        -- apply it to the current context
        vs <- freeVarsToApply x
        reportSDoc "tc.term.def" 30 $ "  free vars:" <+> prettyList_ (map prettyTCM vs)
        let t = defType d
            v = mkTerm vs -- applies x to vs, dropping parameters

        -- Andrea 2019-07-16, Check that the supplied arguments
        -- respect the pure modalities of the current context.
        -- Pure modalities are based on left-division, so it does not
        -- rely on "position" like positional modalities.
        checkModalityArgs d0 vs

        debug vs t v
        return (v, t)
  where
    debug :: Args -> Type -> Term -> TCM ()
    debug vs t v = do
      reportSDoc "tc.term.def" 60 $
        "freeVarsToApply to def " <+> hsep (map (text . show) vs)
      reportSDoc "tc.term.def" 10 $ vcat
        [ "inferred def " <+> prettyTCM x <+> hsep (map prettyTCM vs)
        , nest 2 $ ":" <+> prettyTCM t
        , nest 2 $ "-->" <+> prettyTCM v ]

-- | @checkHeadApplication e t hd args@ checks that @e@ has type @t@,
-- assuming that @e@ has the form @hd args@. The corresponding
-- type-checked term is returned.
--
-- If the head term @hd@ is a coinductive constructor, then a
-- top-level definition @fresh tel = hd args@ (where the clause is
-- delayed) is added, where @tel@ corresponds to the current
-- telescope. The returned term is @fresh tel@.
--
-- Precondition: The head @hd@ has to be unambiguous, and there should
-- not be any need to insert hidden lambdas.
checkHeadApplication :: Comparison -> A.Expr -> Type -> A.Expr -> [NamedArg A.Expr] -> TCM Term
checkHeadApplication cmp e t hd args = do
  SortKit{..} <- sortKit
  sharp <- fmap nameOfSharp <$> coinductionKit
  pOr    <- getNameOfConstrained builtinPOr
  pComp  <- getNameOfConstrained builtinComp
  pHComp <- getNameOfConstrained builtinHComp
  pTrans <- getNameOfConstrained builtinTrans
  mglue  <- getNameOfConstrained builtin_glue
  mglueU  <- getNameOfConstrained builtin_glueU
  case hd of
    A.Def' c s | Just (sz, u) <- isNameOfUniv c -> checkUniv sz u cmp e t c s args

    -- Type checking #. The # that the user can write will be a Def, but the
    -- sharp we generate in the body of the wrapper is a Con.
    A.Def c | Just c == sharp -> checkSharpApplication e t c args

    -- Cubical primitives
    A.Def c | Just c == pComp -> defaultResult' $ Just $ checkPrimComp c
    A.Def c | Just c == pHComp -> defaultResult' $ Just $ checkPrimHComp c
    A.Def c | Just c == pTrans -> defaultResult' $ Just $ checkPrimTrans c
    A.Def c | Just c == pOr   -> defaultResult' $ Just $ checkPOr c
    A.Def c | Just c == mglue -> defaultResult' $ Just $ check_glue c
    A.Def c | Just c == mglueU -> defaultResult' $ Just $ check_glueU c

    _ -> defaultResult
  where
  defaultResult :: TCM Term
  defaultResult = defaultResult' Nothing
  defaultResult' :: Maybe (ArgRanges -> Args -> Type -> TCM Args) -> TCM Term
  defaultResult' mk = do
    (f, t0) <- inferHead hd
    expandLast <- asksTC envExpandLast
    checkArguments cmp expandLast hd args t0 t $ \ st@(ACState cas _fun t1 checkedTarget) -> do
      let check :: Maybe (TCM Args)
          check = do
            k <- mk
            vs <- allApplyElims $ map caElim cas
            pure $ k (map caRange cas) vs t1
      st' <- case check of
               Just ck -> (`setACElims` st) . map Apply <$> ck
               Nothing -> pure st
      v <- unfoldInlined =<< checkHeadConstraints f st'
      coerce' cmp checkedTarget v t1 t

-- Issue #3019 and #4170: Don't insert trailing implicits when checking arguments to existing
-- metavariables.
turnOffExpandLastIfExistingMeta :: A.Expr -> TCM a -> TCM a
turnOffExpandLastIfExistingMeta hd
  | isExistingMeta = reallyDontExpandLast
  | otherwise      = id
  where
    isExistingMeta = isJust $ A.metaNumber =<< metaInfo hd
    metaInfo (A.QuestionMark i _) = Just i
    metaInfo (A.Underscore i)     = Just i
    metaInfo (A.ScopedExpr _ e)   = metaInfo e
    metaInfo _                    = Nothing

-----------------------------------------------------------------------------
-- * Spines
-----------------------------------------------------------------------------

traceCallE :: Call -> ExceptT e TCM r -> ExceptT e TCM r
traceCallE call m = do
  z <- lift $ traceCall call $ runExceptT m
  case z of
    Right e  -> return e
    Left err -> throwError err

-- | If we've already checked the target type we don't have to call coerce.
coerce' :: Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' cmp NotCheckedTarget           v inferred expected = coerce cmp v inferred expected
coerce' cmp (CheckedTarget Nothing)    v _        _        = return v
coerce' cmp (CheckedTarget (Just pid)) v _        expected = blockTermOnProblem expected v pid

-- | Check a list of arguments: @checkArgs args t0 t1@ checks that
--   @t0 = Delta -> t0'@ and @args : Delta@. Inserts hidden arguments to
--   make this happen.  Returns the evaluated arguments @vs@, the remaining
--   type @t0'@ (which should be a subtype of @t1@) and any constraints @cs@
--   that have to be solved for everything to be well-formed.

checkArgumentsE ::
     Comparison
       -- ^ How the inferred type should be compared to the expected result type.
  -> ExpandHidden
       -- ^ Insert trailing hidden arguments?
  -> A.Expr
       -- ^ The function.
  -> [NamedArg A.Expr]
       -- ^ The arguments.
  -> Type
       -- ^ Type of the function.
  -> Maybe Type
       -- ^ Optional: expected result type (type of the whole application).
  -> ExceptT (ArgsCheckState [NamedArg A.Expr]) TCM (ArgsCheckState CheckedTarget)
       -- ^ Upon failure, return the current state for creating a postponed type checking problem.
checkArgumentsE cmp exph hd args t0 t = do
  sPathView <- pathView'
  checkArgumentsE'
    S{ sChecked       = NotCheckedTarget
     , sComp          = cmp
     , sExpand        = exph
     , sFun           = hd
     , sArgs          = zip args $ List.suffixesSatisfying visible args
     , sArgsLen       = length args
     , sFunType       = t0
     , sResultType    = t
     , sSizeLtChecked = False
     , sSkipCheck     = DontSkip
     , sPathView      = sPathView
     }

-- | State used by 'checkArgumentsE''.

data CheckArgumentsE'State = S
  { sChecked :: CheckedTarget
    -- ^ Have we already checked the target?
  , sComp :: Comparison
    -- ^ Comparison to use if checking the target type.
  , sExpand :: ExpandHidden
    -- ^ Insert trailing hidden arguments?
  , sFun :: A.Expr
    -- ^ The function.
  , sArgs :: [(NamedArg A.Expr, Bool)]
    -- ^ Arguments, along with information about whether a given
    -- argument and all remaining arguments are 'visible'.
  , sArgsLen :: !Nat
    -- ^ The length of 'sArgs'.
  , sFunType :: Type
    -- ^ The function's type.
  , sResultType :: Maybe Type
    -- ^ The type of the application.
  , sSizeLtChecked :: !Bool
    -- ^ Have we checked if 'sResultType' is 'BoundedLt'?
  , sSkipCheck :: !SkipCheck
    -- ^ Should the target type check be skipped?
  , sPathView :: Type -> PathView
    -- ^ The function returned by 'pathView''.
  }

-- | Should the target type check in 'checkArgumentsE'' be skipped?

data SkipCheck
  = Skip
  | SkipNext !Nat
    -- ^ Skip the given number of checks.
  | DontSkip

type CheckArgumentsE' = ExceptT (ArgsCheckState [NamedArg A.Expr]) TCM (ArgsCheckState CheckedTarget)

checkArgumentsE'
  :: CheckArgumentsE'State
  -> CheckArgumentsE'

-- Case: no arguments, do not insert trailing hidden arguments: We are done.
checkArgumentsE' S{ sArgs = [], .. }
  | isDontExpandLast sExpand =
    return $ ACState
      { acCheckedArgs = []
      , acFun         = sFun
      , acType        = sFunType
      , acData        = sChecked
      }

-- Case: no arguments, but need to insert trailing hiddens.
checkArgumentsE' S{ sArgs = [], .. } =
  traceCallE (CheckArguments sFun [] sFunType sResultType) $ lift $ do
    sResultType <- traverse (unEl <.> reduce) sResultType
    (ncargs, t) <- implicitCheckedArgs (-1) (\ h _x -> expand sResultType h) sFunType
    return $ ACState
      { acCheckedArgs = map namedThing ncargs
      , acFun         = sFun
      , acType        = t
      , acData        = sChecked
      }
  where
  expand (Just (Pi dom _)) Hidden     = not (hidden dom)
  expand _                 Hidden     = True
  expand (Just (Pi dom _)) Instance{} = not (isInstance dom)
  expand _                 Instance{} = True
  expand _                 NotHidden  = False

-- Case: argument given.
checkArgumentsE'
  s@S{ sArgs = sArgs@((arg@(Arg info e), sArgsVisible) : args), .. } =

    traceCallE (CheckArguments sFun (map fst sArgs) sFunType sResultType) $ do
      lift $ reportSDoc "tc.term.args" 30 $ sep
        [ "checkArgumentsE"
--        , "  sArgs =" <+> prettyA sArgs
        , nest 2 $ vcat
          [ "e (argument) =" <+> prettyA e
          , "sFun         =" <+> prettyA sFun
          , "sFunType     =" <+> prettyTCM sFunType
          , "sResultType  =" <+> maybe "Nothing" prettyTCM sResultType
          ]
        ]
      -- First, insert implicit arguments, depending on current argument @arg@.
      let hx = getHiding info  -- hiding of current argument
          mx :: Maybe ArgName
          mx = bareNameOf e    -- name of current argument
          -- do not insert visible arguments
          expand NotHidden y = False
          -- insert a hidden argument if arg is not hidden or has different name
          -- insert an instance argument if arg is not instance  or has different name
          expand hy        y = not (sameHiding hy hx) || maybe False (y /=) mx
      reportSDoc "tc.term.args" 30 $ vcat
        [ "calling implicitCheckedArgs"
        , nest 2 $ "hx       = " <+> text (show hx)
        , nest 2 $ "mx       = " <+> maybe "nothing" prettyTCM mx
        ]
      (ncargs, sFunType) <- lift $ implicitCheckedArgs (-1) expand sFunType
      -- Separate names from args.
      let (mxs, cargs) = List.unzipWith (\ (Named mx ca) -> (mx, ca)) ncargs
          xs           = catMaybes mxs

      -- We need a function type here, but we don't know which kind
      -- (implicit/explicit). But it might be possible to use injectivity to
      -- force a pi.
      sFunType <- lift $ forcePiUsingInjectivity sFunType

      -- We are done inserting implicit args.  Now, try to check @arg@.
      ifBlocked sFunType
        (\ _ sFunType -> throwError $ ACState
            { acCheckedArgs = cargs
            , acFun         = sFun
            , acType        = sFunType
            , acData        = map fst sArgs
            }) {- else -} $ \ _ sFunType -> do

        -- What can go wrong?

        -- 1. We ran out of function types.
        let shouldBePi =
              -- a) It is an explicit argument, but we ran out of function types.
              if visible info then liftTCM . typeError $ CannotApply sFun sFunType
              -- b) It is an implicit argument, and we did not insert any implicits.
              --    Thus, the type was not a function type to start with.
              else List1.ifNull xs {-then-} (liftTCM . typeError $ CannotApply sFun sFunType)
              -- c) We did insert implicits, but we ran out of implicit function types.
              --    Then, we should inform the user that we did not find his one.
              {-else-} (liftTCM . typeError . WrongNamedArgument arg)

        -- 2. We have a function type left, but it is the wrong one.
        --    Our argument must be implicit, case a) is impossible.
        --    (Otherwise we would have ran out of function types instead.)
        let wrongPi = List1.ifNull xs
              -- b) We have not inserted any implicits.
                {-then-} (liftTCM . typeError $ WrongHidingInApplication sFunType)
              -- c) We inserted implicits, but did not find his one.
                {-else-} (liftTCM . typeError . WrongNamedArgument arg)

        let (skip, next) = case sSkipCheck of
              Skip       -> (True, Skip)
              DontSkip   -> (False, DontSkip)
              SkipNext n -> case compare n 1 of
                LT -> (False, DontSkip)
                EQ -> (True,  DontSkip)
                GT -> (True,  SkipNext (n - 1))

        s <- pure s
          { sFun       = A.App (A.defaultAppInfo $ getRange (sFun, arg)) sFun arg
          , sArgs      = args
          , sArgsLen   = sArgsLen - 1
          , sFunType   = sFunType
          , sSkipCheck = next
          }

        -- Check the target type if we can get away with it.
        s <- lift $
          case (sChecked, skip, sResultType) of
            (NotCheckedTarget, False, Just sResultType) | sArgsVisible -> do
              -- How many visible Π's (up to at most sArgsLen) does
              -- sFunType start with?
              TelV tel tgt <- telViewUpTo' sArgsLen visible sFunType
              let visiblePis = size tel

                  -- The free variables less than visiblePis in tgt.
                  freeInTgt =
                    fst $ VarSet.split visiblePis $ freeVars tgt

              rigid <- isRigid s tgt
              -- The target must be rigid.
              case rigid of
                IsNotRigid reason ->
                      -- Skip the next visiblePis - 1 - k checks.
                  let skip k   = s{ sSkipCheck =
                                    SkipNext $ visiblePis - 1 - k
                                  }
                      dontSkip = s
                  in return $ case reason of
                    Permanent   -> skip 0
                    Unspecified -> dontSkip
                    AVar x      ->
                      if x `VarSet.member` freeInTgt
                      then skip x
                      else skip 0
                IsRigid -> do
                  -- Andreas, 2024-03-01, issue #7158 reported by Amy.
                  -- We need to check that the arity of the function type
                  -- is sufficient before checking the target,
                  -- otherwise the target is non-sensical.
                  if visiblePis < sArgsLen then return s else do

                      -- Is any free variable in tgt less than
                      -- visiblePis?
                  let dep = not (null freeInTgt)
                  -- The target must be non-dependent.
                  if dep then return s else do

                  -- Andreas, 2019-03-28, issue #3248:
                  -- If the target type is SIZELT, we need coerce, leqType is insufficient.
                  -- For example, we have i : Size <= (Size< ↑ i), but not Size <= (Size< ↑ i).
                  (isSizeLt, sResultType, s) <-
                    if sSizeLtChecked
                    then return (False, sResultType, s)
                    else do
                      sResultType <- reduce sResultType
                      isSizeLt    <- isSizeType sResultType <&> \case
                        Just (BoundedLt _) -> True
                        _                  -> False
                      return ( isSizeLt
                             , sResultType
                             , s{ sResultType    = Just sResultType
                                , sSizeLtChecked = True
                                , sSkipCheck     =
                                    if isSizeLt then Skip else DontSkip
                                }
                             )
                  if isSizeLt then return s else do

                  let tgt1 = applySubst
                               (strengthenS impossible visiblePis)
                               tgt
                  reportSDoc "tc.term.args.target" 30 $ vcat
                    [ "Checking target types first"
                    , nest 2 $ "inferred =" <+> prettyTCM tgt1
                    , nest 2 $ "expected =" <+> prettyTCM sResultType ]
                  chk <-
                    traceCall
                      (CheckTargetType
                         (fuseRange sFun sArgs) tgt1 sResultType) $
                      CheckedTarget <$>
                        ifNoConstraints_ (compareType sComp tgt1 sResultType)
                          (return Nothing) (return . Just)
                  return s{ sChecked = chk }

            _ -> return s

        -- sFunType <- lift $ forcePi (getHiding info)
        --                  (maybe "_" rangedThing $ nameOf e) sFunType
        case unEl sFunType of
          Pi (Dom{domInfo = info', domName = dname, unDom = a}) b
            | let name = bareNameWithDefault "_" dname,
              sameHiding info info'
              && (visible info || maybe True (name ==) mx) -> do
                u <- lift $ applyModalityToContext info' $ do
                 -- Andreas, 2014-05-30 experiment to check non-dependent arguments
                 -- after the spine has been processed.  Allows to propagate type info
                 -- from ascribed type into extended-lambdas.  Would solve issue 1159.
                 -- However, leaves unsolved type checking problems in the test suite.
                 -- I do not know what I am doing wrong here.
                 -- Could be extreme order-sensitivity or my abuse of the postponing
                 -- mechanism.
                 -- Andreas, 2016-02-02: Ulf says unless there is actually some meta
                 -- blocking a postponed type checking problem, we might never retry,
                 -- since the trigger for retrying constraints is solving a meta.
                 -- Thus, the following naive use violates some invariant.
                 -- if not $ isBinderUsed b
                 -- then postponeTypeCheckingProblem (CheckExpr (namedThing e) a) (return True) else
                  let e' = e { nameOf = (nameOf e) <|> dname }
                  checkNamedArg (Arg info' e') a

                c <- lift $ makeLockConstraint sFunType u
                -- save relevance info' from domain in argument
                let ca = CheckedArg{ caElim = Apply (Arg info' u), caRange = getRange e, caConstraint = c }
                addCheckedArgs cargs ca $
                  checkArgumentsE' s{ sFunType = absApp b u }
            | otherwise -> do
                reportSDoc "error" 10 $ nest 2 $ vcat
                  [ text $ "info      = " ++ show info
                  , text $ "info'     = " ++ show info'
                  , text $ "absName b = " ++ absName b
                  , text $ "nameOf e  = " ++ show (nameOf e)
                  ]
                wrongPi
          _
            | visible info
            , PathType sort _ _ bA x y <- sPathView sFunType -> do
                lift $ reportSDoc "tc.term.args" 30 $ text $ show bA
                u <- lift $ checkExpr (namedThing e) =<< primIntervalType
                let ca = CheckedArg
                     { caElim       = IApply (unArg x) (unArg y) u
                     , caRange      = getRange e
                     , caConstraint = Nothing
                     }
                addCheckedArgs cargs ca $
                  checkArgumentsE'
                    s{ sChecked = NotCheckedTarget
                     , sFunType = El sort $ unArg bA `apply` [argN u]
                     }
          _ -> shouldBePi
  where
    addCheckedArgs ::
         [CheckedArg]
      -> CheckedArg
      -> CheckArgumentsE'
      -> CheckArgumentsE'
    addCheckedArgs cas ca cont = do
      let upd :: ArgsCheckState a -> ArgsCheckState a
          upd st = st{ acCheckedArgs = cas ++ ca : acCheckedArgs st }
      -- Add checked arguments to both regular and exceptional result of @cont@.
      withError upd $ upd <$> cont

-- | The result of 'isRigid'.

data IsRigid
  = IsRigid
    -- ^ The type is rigid.
  | IsNotRigid !IsPermanent
    -- ^ The type is not rigid. If the argument is 'Nothing', then
    -- this will not change. If the argument is @'Just' reason@, then
    -- this might change for the given @reason@.

-- | Is the result of 'isRigid' \"permanent\"?

data IsPermanent
  = Permanent
    -- ^ Yes.
  | AVar !Nat
    -- ^ The result does not change unless the given variable is
    -- instantiated.
  | Unspecified
    -- ^ Maybe, maybe not.

-- | Is the type \"rigid\"?

isRigid :: CheckArgumentsE'State -> Type -> TCM IsRigid
isRigid s t | PathType{} <- sPathView s t =
  -- Path is not rigid.
  return $ IsNotRigid Permanent
isRigid _ (El _ t) = case t of
  Var x _    -> return $ IsNotRigid (AVar x)
  Lam{}      -> return $ IsNotRigid Permanent
  Lit{}      -> return $ IsNotRigid Permanent
  Con{}      -> return $ IsNotRigid Permanent
  Pi dom _   -> return $
                if visible dom then IsRigid else IsNotRigid Permanent
  Sort{}     -> return $ IsNotRigid Permanent
  Level{}    -> return $ IsNotRigid Permanent
  MetaV{}    -> return $ IsNotRigid Unspecified
  DontCare{} -> return $ IsNotRigid Permanent
  Dummy{}    -> return $ IsNotRigid Permanent
  Def d _    -> getConstInfo d <&> theDef <&> \case
    Axiom{}                   -> IsRigid
    DataOrRecSig{}            -> IsRigid
    AbstractDefn{}            -> IsRigid
    Function{funClauses = cs} -> if null cs
                                 then IsRigid
                                 else IsNotRigid Unspecified
                                      -- This Reason could perhaps be
                                      -- more precise (in some cases).
    Datatype{}                -> IsRigid
    Record{}                  -> IsRigid
    Constructor{}             -> __IMPOSSIBLE__
    GeneralizableVar{}        -> __IMPOSSIBLE__
    Primitive{}               -> IsNotRigid Unspecified
    PrimitiveSort{}           -> IsNotRigid Unspecified

-- | Check that a list of arguments fits a telescope.
--   Inserts hidden arguments as necessary.
--   Returns the type-checked arguments and the remaining telescope.
checkArguments_
  :: Comparison           -- ^ Comparison for target
  -> ExpandHidden         -- ^ Eagerly insert trailing hidden arguments?
  -> A.Expr               -- ^ Function.
  -> [NamedArg A.Expr]    -- ^ Arguments to check.
  -> Telescope            -- ^ Telescope to check arguments against.
  -> TCM (Elims, Telescope)
     -- ^ Checked arguments and remaining telescope if successful.
checkArguments_ cmp exh fun args tel = postponeInstanceConstraints $ do
    z <- runExceptT $
      checkArgumentsE cmp exh fun args (telePi tel __DUMMY_TYPE__) Nothing
    case z of
      Right (ACState cas _ t _) -> do
        es <- noHeadConstraints cas
        let TelV tel' _ = telView' t
        return (es, tel')
      Left _ -> __IMPOSSIBLE__  -- type cannot be blocked as it is generated by telePi

-- | @checkArguments cmp exph hd args t0 t k@ tries @checkArgumentsE cmp exph hd args t0 t@.
-- If it succeeds, it continues @k@ with the returned results.  If it fails,
-- it registers a postponed typechecking problem and returns the resulting new
-- meta variable.
--
-- Checks @e := ((hd : t0) args) : t@.
checkArguments ::
     Comparison
       -- ^ How the inferred type should be compared to the expected result type.
  -> ExpandHidden
       -- ^ Insert trailing hidden arguments?
  -> A.Expr
       -- ^ The function (a head).
  -> [NamedArg A.Expr]
       -- ^ The arguments to check.
  -> Type
       -- ^ Type of the function.
  -> Type
       -- ^ Expected result type (type of the whole application).
  -> (ArgsCheckState CheckedTarget -> TCM Term)
       -- ^ Continuation receiving the check arguments.
  -> TCM Term
checkArguments cmp exph hd args t0 t k = postponeInstanceConstraints $ do
  z <- runExceptT $ checkArgumentsE cmp exph hd args t0 (Just t)
  case z of
    Right st -> k st
    Left problem -> postponeArgs problem cmp exph hd args t0 t k
      -- if unsuccessful, postpone checking until t0 unblocks

postponeArgs ::
     (ArgsCheckState [NamedArg A.Expr])
       -- ^ The last sound state of the arguments checker.
  -> Comparison
       -- ^ How the inferred type should be compared to the expected result type.
  -> ExpandHidden
       -- ^ Insert trailing hidden arguments?
  -> A.Expr
       -- ^ The original function (a head).
  -> [NamedArg A.Expr]
       -- ^ The original arguments to check.
  -> Type
       -- ^ Type of the original function.
  -> Type
       -- ^ Expected result type (type of the whole application).
  -> (ArgsCheckState CheckedTarget -> TCM Term)
       -- ^ Continuation receiving the check arguments.
  -> TCM Term
postponeArgs (ACState cas fun t1 es) cmp exph hd args t0 t k = do
  reportSDoc "tc.term.expr.args" 80 $
    sep [ "postponed checking arguments"
        , nest 4 $ prettyList (map (prettyA . namedThing . unArg) args)
        , nest 2 $ "against"
        , nest 4 $ prettyTCM t0
        ] $$
    sep [ "progress:"
        , nest 2 $ "checked" <+> prettyList (map (prettyTCM . caElim) cas)
        , nest 2 $ "remaining" <+> sep
            [ prettyList (map (prettyA . namedThing . unArg) es)
            , nest 2 $ ":" <+> prettyTCM t1
            ]
        ]
  postponeTypeCheckingProblem_ $
    CheckArgs cmp exph fun es t1 t $ \ (ACState cas' func t pid) ->
      k $ ACState (cas ++ cas') func t pid

-----------------------------------------------------------------------------
-- * Constructors
-----------------------------------------------------------------------------

-- | Check the type of a constructor application. This is easier than
--   a general application since the implicit arguments can be inserted
--   without looking at the arguments to the constructor.
checkConstructorApplication ::
  Comparison
       -- ^ How the inferred type of the application should be compared to the expected type.
  -> A.Expr
       -- ^ The whole application expression.
  -> Type
       -- ^ The expected type of the whole application.
  -> ConHead
       -- ^ The head of the application.
  -> A.Expr
       -- ^ The original head of the application.
  -> [NamedArg A.Expr]
       -- ^ The arguments.
  -> TCM Term
checkConstructorApplication cmp org t c hd args = do
  reportSDoc "tc.term.con" 50 $ vcat
    [ "entering checkConstructorApplication"
    , nest 2 $ vcat
      [ "org  =" <+> prettyTCM org
      , "t    =" <+> prettyTCM t
      , "c    =" <+> prettyTCM c
      , "args =" <+> do prettyList $ fmap prettyTCM args
    ] ]

  cdef  <- getConInfo c

  checkModality (conName c) cdef

  let paramsGiven = checkForParams args
  if paramsGiven then fallback else do
    reportSDoc "tc.term.con" 50 $ "checkConstructorApplication: no parameters explicitly supplied, continuing..."

    let Constructor{conData = d, conPars = npars} = theDef cdef
    reportSDoc "tc.term.con" 50 $ nest 2 $ "d    =" <+> prettyTCM d
    -- Issue 661: t maybe an evaluated form of d .., so we evaluate d
    -- as well and then check wether we deal with the same datatype
    t0 <- reduce (Def d [])
    tReduced <- reduce t
    case (t0, unEl tReduced) of -- Only fully applied constructors get special treatment
      (Def d0 _, Def d' es) -> do
        let ~(Just vs) = allApplyElims es
        reportSDoc "tc.term.con" 50 $ nest 2 $ "d0   =" <+> prettyTCM d0
        reportSDoc "tc.term.con" 50 $ nest 2 $ "d'   =" <+> prettyTCM d'
        reportSDoc "tc.term.con" 50 $ nest 2 $ "vs   =" <+> prettyTCM vs
        if d' /= d0 then fallback else do
         -- Issue 661: d' may take more parameters than d, in particular
         -- these additional parameters could be a module parameter telescope.
         -- Since we get the constructor type ctype from d but the parameters
         -- from t = Def d' vs, we drop the additional parameters.
         npars' <- getNumberOfParameters d'
         caseMaybe (sequenceA $ Pair (Just npars) npars') fallback $ \ (Pair n n') -> do
           reportSDoc "tc.term.con" 50 $ nest 2 $ text $ "n    = " ++ show n
           reportSDoc "tc.term.con" 50 $ nest 2 $ text $ "n'   = " ++ show n'
           when (n > n')  -- preprocessor does not like ', so put on next line
             __IMPOSSIBLE__
           let ps    = take n $ drop (n' - n) vs
               ctype = defType cdef
           reportSDoc "tc.term.con" 20 $ vcat
             [ "special checking of constructor application of" <+> prettyTCM c
             , nest 2 $ vcat [ "ps     =" <+> prettyTCM ps
                             , "ctype  =" <+> prettyTCM ctype ] ]
           let ctype' = ctype `piApply` ps
           reportSDoc "tc.term.con" 20 $ nest 2 $ "ctype' =" <+> prettyTCM ctype'
           -- get the parameter names
           let TelV ptel _ = telView'UpTo n ctype
           let pnames = map (fmap fst) $ telToList ptel
           -- drop the parameter arguments
               args' = dropArgs pnames args
           -- check the non-parameter arguments
           expandLast <- asksTC envExpandLast
           checkArguments cmp expandLast hd args' ctype' t \ st@(ACState _ _ t' targetCheck) -> do
             reportSDoc "tc.term.con" 20 $ nest 2 $ vcat
               [ text "es     =" <+> prettyTCM es
               , text "t'     =" <+> prettyTCM t' ]
             v <- checkHeadConstraints (Con c ConOCon) st
             coerce' cmp targetCheck v t' t
      _ -> do
        reportSDoc "tc.term.con" 50 $ nest 2 $ "we are not at a datatype, falling back"
        fallback
  where
    fallback = checkHeadApplication cmp org t (A.Con (unambiguous $ conName c)) args

    -- Check if there are explicitly given hidden arguments,
    -- in which case we fall back to default type checking.
    -- We could work harder, but let's not for now.
    --
    -- Andreas, 2012-04-18: if all inital args are underscores, ignore them
    checkForParams args =
      let (hargs, rest) = break visible args
          notUnderscore A.Underscore{} = False
          notUnderscore _              = True
      in  any (notUnderscore . unScope . namedArg) hargs

    -- Drop the constructor arguments that correspond to parameters.
    dropArgs [] args                = args
    dropArgs ps []                  = args
    dropArgs ps args@(arg : args')
      | Just p   <- name,
        Just ps' <- namedPar p ps   = dropArgs ps' args'
      | Nothing  <- name,
        Just ps' <- unnamedPar h ps = dropArgs ps' args'
      | otherwise                   = args
      where
        name = bareNameOf arg
        h    = getHiding arg

        namedPar   x = dropPar ((x ==) . unDom)
        unnamedPar h = dropPar (sameHiding h)

        dropPar this (p : ps) | this p    = Just ps
                              | otherwise = dropPar this ps
        dropPar _ [] = Nothing

-- | Return an unblocking action in case of failure.
type DisambiguateConstructor = TCM (Either (Blocker, ConstructorDisambiguationData) ConHead)

-- | Successfully disambiguate constructor with given choice.
decideOn :: ConHead -> DisambiguateConstructor
decideOn c = do
  reportSLn "tc.check.term.con" 40 $ "  decided on: " ++ prettyShow c
  storeDisambiguatedConstructor (conInductive c) (conName c)
  return $ Right c

-- | Returns an unblocking action in case of failure.
disambiguateConstructor :: List1 QName -> A.Args -> Type -> DisambiguateConstructor
disambiguateConstructor cs0 args t = do
  reportSLn "tc.check.term.con" 40 $ "Ambiguous constructor: " ++ prettyShow cs0
  reportSDoc "tc.check.term.con" 40 $ vcat $ "Arguments:" : map (nest 2 . prettyTCM) args

  -- Get the datatypes of the various constructors
  let getData Constructor{conData = d} = d
      getData _                        = __IMPOSSIBLE__
  reportSLn "tc.check.term.con" 40 $ "  ranges before: " ++ prettyShow (getRange cs0)
  -- We use the reduced constructor when disambiguating, but
  -- the original constructor for type checking. This is important
  -- since they may have different types (different parameters).
  -- See issue 279.
  -- Andreas, 2017-08-13, issue #2686: ignore abstract constructors
  ccons  <- List1.rights <$> do
     forM cs0 $ \ c -> mapRight (c,) <$> getConForm c
  reportSLn "tc.check.term.con" 40 $ "  reduced: " ++ prettyShow (map snd ccons)
  case ccons of
    []    -> typeError $ AbstractConstructorNotInScope $ List1.head cs0
    [(c0,con)] -> do
      let c = setConName c0 con
      reportSLn "tc.check.term.con" 40 $ "  only one non-abstract constructor: " ++ prettyShow c
      decideOn c
    cons@(c0,_):conss   -> do
      dcs :: List1 (QName, Type, ConHead) <- forM (cons :| conss) $ \ (c, con) -> do
        t   <- defType <$> getConstInfo c
        def <- getConInfo con
        pure (getData (theDef def), t, setConName c con)
      resolveAmbiguousConstructor $ ConstructorDisambiguationData c0 dcs args t

-- | Retry a constructor disambiguation.
disambiguateConstructor' :: ConstructorDisambiguationData -> (ConHead -> TCM Term) -> TCM Term
disambiguateConstructor' bcd cont = do
  afterDisambiguation cont $ resolveAmbiguousConstructor bcd

-- | Postpone a failing disambiguation or call given continuation.
afterDisambiguation :: (ConHead -> TCM Term) -> DisambiguateConstructor -> TCM Term
afterDisambiguation cont run =
  run >>= \case
    Left (unblock, bcd) -> postponeTypeCheckingProblem (DisambiguateConstructor bcd cont) unblock
    Right c -> cont c

-- | Resolve ambiguous constructor by looking at target type and argument skeleton.
resolveAmbiguousConstructor :: ConstructorDisambiguationData -> DisambiguateConstructor
resolveAmbiguousConstructor bcd@(ConstructorDisambiguationData c0 dcs1 args t) = do
      let dcs = List1.toList dcs1

      -- Lets look at the target type at this point
      TelV tel t1 <- telViewPath t
      addContext tel $ do
       reportSDoc "tc.check.term.con" 40 $ nest 2 $
         "target type: " <+> prettyTCM t1
       -- If we don't have a target type yet, try to look at the argument types.
       ifBlocked t1 (\ b _ -> disambiguateByArgs dcs args $ postpone b) $ \ _ t' ->
         caseMaybeM (isDataOrRecord $ unEl t') (badCon t') $ \ (d, _) -> do
           let dcs' = filter ((d ==) . fst3) dcs
           case map thd3 dcs' of
             [c] -> decideOn c
             []  -> badCon $ t' $> Def d []
             -- If the information from the target type did not eliminate ambiguity fully,
             -- try to further eliminate alternatives by looking at the arguments.
             c:cs-> disambiguateByArgs dcs' args $
                      typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d $
                        fmap conName $ c :| cs
  where
    postpone b = return $ Left (b, bcd)
    badCon t = typeError $ ConstructorDoesNotTargetGivenType c0 t

-- | Disambiguate constructor by looking at its arguments.
--
-- Look at simple visible arguments (variables (bound and generalizable ones) and defined names).
-- From these we can compute an approximate type effortlessly:
-- 1. Throw away hidden domains (needed for generalizable variables).
-- 2. If the remainder is a defined name that is not blocked on anything, we take this name as
--    approximate type of the argument.
-- This gives us a skeleton @[Maybe QName]@.  Compute the same from the constructor types
-- of the candidates and see if we find any mismatches that allow us to rule out the candidate.
disambiguateByArgs :: [(QName, Type, ConHead)] -> A.Args -> DisambiguateConstructor -> DisambiguateConstructor
disambiguateByArgs dcs args fallback = do

    -- Look for visible arguments that are just variables,
    -- so that we can get their type directly from the context
    -- without full-fledged type inference.
    askel <- visibleVarArgs
    reportSDoc "tc.check.term.con" 40 $ hsep $
      "trying disambiguation by arguments" : map prettyTCM askel
    reportSDoc "tc.check.term.con" 80 $ hsep $
      "trying disambiguation by arguments" : map pretty askel

    -- Filter out candidates with definitive mismatches.
    cands <- filterM (\ (_d, t, _c) -> matchSkel askel =<< visibleConDoms t) dcs
    case cands of
      [(_d, _t, c)] -> decideOn c
      _ -> fallback
    where

    -- @match@ is successful if there no name conflict (q ≠ q')
    -- and the argument skeleton is not longer thatn the constructor skeleton.
    match ::
          [Maybe QName]   -- Specification (argument skeleton).
       -> [Maybe QName]   -- Candidate (constructor skeleton).
       -> Bool
    match = curry $ \case
      ([], _ ) -> True
      (_ , []) -> False
      (Just q : ms, Just q' : ms') -> q == q' && match ms ms'
      (_ : ms, _ : ms') -> match ms ms'

    -- @match@ with debug printing.
    matchSkel :: [Maybe QName] -> [Maybe QName] -> TCM Bool
    matchSkel argsSkel conSkel = do
      let res = match argsSkel conSkel
      reportSDoc "tc.check.term.con" 40 $ vcat
        [ "matchSkel returns" <+> pretty res <+> "on:"
        , nest 2 $ pretty argsSkel
        , nest 2 $ pretty conSkel
        ]
      return res

    -- Only look at visible arguments that are variables or similar identifiers.
    -- For variables/symbols @Just getTypeHead@ else @Nothing@.
    visibleVarArgs :: TCM [Maybe QName]
    visibleVarArgs = forM (filter visible args) $ \ (arg :: NamedArg A.Expr) -> do
        let v = unScope $ namedArg arg
        reportSDoc "tc.check.term.con" 40 $ "is this a variable? :" <+> prettyTCM v
        reportSDoc "tc.check.term.con" 90 $ "is this a variable? :" <+> (text . show) v
        case v of

          -- We can readly grab the type of a variable from the context.
          A.Var x -> do
            t <- unDom . snd <$> getVarInfo x
            reportSDoc "tc.check.term.con" 40 $ "type of variable:" <+> prettyTCM t
            -- Just keep the name @D@ of type @D vs@
            getTypeHead t

          -- We can also grab the type of defined symbols if we find them in the signature.
          A.Def x -> do
            getConstInfo' x >>= \case
              Right def -> getTypeHead $ defType def
              Left{} -> return Nothing
          _ -> return Nothing

    -- List of visible arguments of the constructor candidate.
    -- E.g. vcons : {A : Set} {n : Nat} (x : A) (xs : Vec A n) → Vec A (suc n)
    -- becomes vcons : ? → Vec → .
    visibleConDoms :: Type -> TCM [Maybe QName]
    visibleConDoms t = do
      TelV tel _ <- telViewPath t
      mapM (getTypeHead . snd . unDom) $ filter visible $ telToList tel

-- | If type is of the form @F vs@ and not blocked in any way, return @F@.
getTypeHead :: Type -> TCM (Maybe QName)
getTypeHead t = do
  res <- ifBlocked t (\ _ _ -> return Nothing) $ \ nb t -> do
    case nb of
      ReallyNotBlocked -> do
        -- Drop initial hidden domains (only needed for generalizable variables).
        TelV _ core <- telViewUpTo' (negate 1) (not . visible) t
        case unEl core of
          Def q _ -> return $ Just q
          _ -> return Nothing
      -- In the other cases, we do not get the data name.
      _ -> return Nothing
  reportSDoc "tc.check.term.con" 80 $ hcat $ "getTypeHead(" : prettyTCM t : ") = " : pretty res : []
  return res


---------------------------------------------------------------------------
-- * Projections
---------------------------------------------------------------------------

checkUnambiguousProjectionApplication :: Comparison -> A.Expr -> Type -> QName -> ProjOrigin -> A.Expr -> [NamedArg A.Expr] -> TCM Term
checkUnambiguousProjectionApplication cmp e t x o hd args = do
  let fallback = checkHeadApplication cmp e t hd args
  -- Andreas, 2021-02-19, issue #3289
  -- If a postfix projection was moved to the head by appView,
  -- we have to patch the first argument with the correct hiding info.
  case (o, args) of
    (ProjPostfix, arg : rest) -> do
      -- Andreas, 2021-11-19, issue #5657:
      -- If @x@ has been brought into scope by e.g. @open R r@, it is no longer
      -- a projection even though the scope checker labels it so.
      -- Thus, @isProjection@ may fail.
      caseMaybeM (isProjection x) fallback $ \ pr -> do
        checkHeadApplication cmp e t hd (setArgInfo (projArgInfo pr) arg : rest)
    _ -> fallback

-- | Inferring the type of an overloaded projection application.
--   See 'inferOrCheckProjApp'.

inferProjApp :: A.Expr -> ProjOrigin -> List1 QName -> A.Expr -> A.Args -> TCM (Term, Type)
inferProjApp e o ds hd args0 = do
  (v, t, _) <- inferOrCheckProjApp e o ds hd args0 Nothing
  return (v, t)

-- | Checking the type of an overloaded projection application.
--   See 'inferOrCheckProjApp'.

checkProjApp  :: Comparison -> A.Expr -> ProjOrigin -> List1 QName -> A.Expr -> A.Args -> Type -> TCM Term
checkProjApp cmp e o ds hd args0 t = do
  (v, ti, targetCheck) <- inferOrCheckProjApp e o ds hd args0 (Just (cmp, t))
  coerce' cmp targetCheck v ti t

-- | Checking the type of an overloaded projection application.
--   See 'inferOrCheckProjAppToKnownPrincipalArg'.

checkProjAppToKnownPrincipalArg ::
  Comparison
  -> A.Expr
  -> ProjOrigin
  -> List1 QName
  -> A.Expr
  -> A.Args
  -> Type
  -> Int
  -> Term
  -> Type
  -> PrincipalArgTypeMetas
  -> TCM Term
checkProjAppToKnownPrincipalArg cmp e o ds hd args0 t k v0 pt patm = do
  (v, ti, targetCheck) <- inferOrCheckProjAppToKnownPrincipalArg e o ds hd args0 (Just (cmp, t)) k v0 pt (Just patm)
  coerce' cmp targetCheck v ti t

-- | Inferring or Checking an overloaded projection application.
--
--   The overloaded projection is disambiguated by inferring the type of its
--   principal argument, which is the first visible argument.

inferOrCheckProjApp
  :: A.Expr
     -- ^ The whole expression which constitutes the application.
  -> ProjOrigin
     -- ^ The origin of the projection involved in this projection application.
  -> List1 QName
     -- ^ The projection name (potentially ambiguous).
  -> A.Expr
     -- ^ The projection as expression.
  -> A.Args
     -- ^ The arguments to the projection.
  -> Maybe (Comparison, Type)
     -- ^ The expected type of the expression (if 'Nothing', infer it).
  -> TCM (Term, Type, CheckedTarget)
     -- ^ The type-checked expression and its type (if successful).
inferOrCheckProjApp e o ds hd args mt = do
  reportSDoc "tc.proj.amb" 20 $ vcat
    [ "checking ambiguous projection"
    , text $ "  ds   = " ++ prettyShow ds
    , text   "  args = " <+> do prettyList $ fmap prettyTCM args
    , text   "  t    = " <+> caseMaybe mt "Nothing" prettyTCM
    ]

  let cmp = caseMaybe mt CmpEq fst

      -- Postpone the whole type checking problem
      -- if type of principal argument (or the type where we get it from)
      -- is blocked by meta m.
      postpone b = do
        tc <- caseMaybe mt newTypeMeta_ (return . snd)
        v <- postponeTypeCheckingProblem (CheckExpr cmp e tc) b
        return (v, tc, NotCheckedTarget)

  -- The following cases need to be considered:
  -- 1. No arguments to the projection.
  -- 2. Arguments (parameters), but not the principal argument.
  -- 3. Argument(s) including the principal argument.

  -- For now, we only allow ambiguous projections if the first visible
  -- argument is the record value.

  case filter (visible . snd) $ zip [0..] args of

    -- Case: we have no visible argument to the projection.
    -- In inference mode, we really need the visible argument, postponing does not help
    [] -> caseMaybe mt (refuseProjNotApplied ds) $ \ (cmp , t) -> do
      -- If we have the type, we can try to get the type of the principal argument.
      -- It is the first visible argument.
      TelV _ptel core <- telViewUpTo' (-1) (not . visible) t
      ifBlocked core (\ m _ -> postpone m) $ {-else-} \ _ core -> do
      ifNotPiType core (\ _ -> refuseProjNotApplied ds) $ {-else-} \ dom _b -> do
      ifBlocked (unDom dom) (\ m _ -> postpone m) $ {-else-} \ _ ta -> do
      caseMaybeM (isRecordType ta) (refuseProjNotRecordType ds Nothing ta)
        \ (_q, _pars, RecordData{ _recFields = fs }) -> do
          case forMaybe fs $ \ f -> Fold.find (unDom f ==) ds of
            [] -> refuseProjNoMatching ds
            [d] -> do
              storeDisambiguatedProjection d
              -- checkHeadApplication will check the target type
              (, t, CheckedTarget Nothing) <$>
                checkHeadApplication cmp e t (A.Proj o $ unambiguous d) args
            _ -> __IMPOSSIBLE__

    -- Case: we have a visible argument
    ((k, arg) : _) -> do
      (v0, ta) <- inferExpr $ namedArg arg
      reportSDoc "tc.proj.amb" 25 $ vcat
        [ "  principal arg " <+> prettyTCM arg
        , "  has type "      <+> prettyTCM ta
        ]
      inferOrCheckProjAppToKnownPrincipalArg e o ds hd args mt k v0 ta Nothing

-- | Same arguments 'inferOrCheckProjApp' above but also gets the position,
--   value and type of the principal argument.
inferOrCheckProjAppToKnownPrincipalArg
  :: A.Expr
     -- ^ The whole expression which constitutes the application.
  -> ProjOrigin
     -- ^ The origin of the projection involved in this projection application.
  -> List1 QName
     -- ^ The projection name (potentially ambiguous).
  -> A.Expr
     -- ^ The projection (as application head).
  -> A.Args
     -- ^ The arguments to the projection.
  -> Maybe (Comparison, Type)
     -- ^ The expected type of the expression (if 'Nothing', infer it).
  -> Int
     -- ^ The position of the principal argument.
  -> Term
     -- ^ The value of the principal argument.
  -> Type
     -- ^ The type of the principal argument.
  -> Maybe PrincipalArgTypeMetas
     -- ^ The metas previously created for the principal argument's type, when
     --   picking up a postponed problem. 'Nothing', otherwise.
  -> TCM (Term, Type, CheckedTarget)
     -- ^ The type-checked expression and its type (if successful).
inferOrCheckProjAppToKnownPrincipalArg e o ds hd args mt k v0 ta mpatm = do
  let cmp = caseMaybe mt CmpEq fst
      postpone b patm = do
        tc <- caseMaybe mt newTypeMeta_ (return . snd)
        v <- postponeTypeCheckingProblem (CheckProjAppToKnownPrincipalArg cmp e o ds hd args tc k v0 ta patm) b
        return (v, tc, NotCheckedTarget)
  -- ta should be a record type (after introducing the hidden args in v0)
  patm@(PrincipalArgTypeMetas vargs ta) <- case mpatm of
    -- keep using the previously created metas, when picking up a postponed
    -- problem - see #4924
    Just patm -> return patm
    -- create fresh metas
    Nothing -> uncurry PrincipalArgTypeMetas <$> implicitArgs (-1) (not . visible) ta
  let v = v0 `apply` vargs
  ifBlocked ta (\ m _ -> postpone m patm) {-else-} $ \ _ ta -> do
  caseMaybeM (isRecordType ta) (refuseProjNotRecordType ds (Just v0) ta) $ \ (q, _pars0, _) -> do

      -- try to project it with all of the possible projections
      let try d = do
            reportSDoc "tc.proj.amb" 30 $ vcat
              [ text $ "trying projection " ++ prettyShow d
              , "  td  = " <+> caseMaybeM (getDefType d ta) "Nothing" prettyTCM
              ]

            -- get the original projection name
            def <- lift $ getConstInfo d
            let isP = isProjection_ $ theDef def
            reportSDoc "tc.proj.amb" 40 $ vcat $
              text ( "  isProjection = " ++ caseMaybe isP "no" (const "yes")
                   ) : caseMaybe isP [] (\ Projection{ projProper = proper, projOrig = orig } ->
              [ text $ "  proper       = " ++ show proper
              , text $ "  orig         = " ++ prettyShow orig
              ])

            -- Andreas, 2017-01-21, issue #2422
            -- The scope checker considers inherited projections (from nested records)
            -- as projections and allows overloading.  However, since they are defined
            -- as *composition* of projections, the type checker does *not* recognize them,
            -- and @isP@ will be @Nothing@.
            -- However, we can ignore this, as we only need the @orig@inal projection name
            -- for removing false ambiguity.  Thus, we skip these checks:

            -- Projection{ projProper = proper, projOrig = orig } <- MaybeT $ return isP
            -- guard $ isJust proper
            let orig = caseMaybe isP d projOrig

            -- try to eliminate
            (dom, u, tb) <- MaybeT (projectTyped v ta o d `catchError` \ _ -> return Nothing)
            reportSDoc "tc.proj.amb" 30 $ vcat
              [ "  dom = " <+> prettyTCM dom
              , "  u   = " <+> prettyTCM u
              , "  tb  = " <+> prettyTCM tb
              ]
            (q', pars, _) <- MaybeT $ isRecordType $ unDom dom
            reportSDoc "tc.proj.amb" 30 $ vcat
              [ "  q   = " <+> prettyTCM q
              , "  q'  = " <+> prettyTCM q'
              ]
            guard (q == q')
            -- Get the type of the projection and check
            -- that the first visible argument is the record value.
            let tfull = defType def
            TelV tel _ <- lift $ telViewUpTo' (-1) (not . visible) tfull
            reportSDoc "tc.proj.amb" 30 $ vcat
              [ text $ "  size tel  = " ++ show (size tel)
              , text $ "  size pars = " ++ show (size pars)
              ]
            -- See issue 1960 for when the following assertion fails for
            -- the correct disambiguation.
            -- guard (natSize tel == natSize pars)

            guard =<< do isNothing <$> do lift $ checkModality' d def
            return (orig, (d, (pars, (dom, u, tb))))

      cands <- List1.groupOn fst . List1.catMaybes <$> mapM (runMaybeT . try) ds
      case cands of
        [] -> refuseProjNoMatching ds
        (_:_:_) -> refuseProj ds $ fwords "several matching candidates can be applied."
        -- case: just one matching projection d
        -- the term u = d v
        -- the type tb is the type of this application
        [ (_orig, (d, (pars, (_dom,u,tb)))) :| _ ] -> do
          storeDisambiguatedProjection d

          -- Check parameters
          tfull <- typeOfConst d
          (args0, princArg : args') <- pure $ splitAt k args
          (_,_) <- checkKnownArguments args0 pars tfull

          -- Check remaining arguments
          let
            fun = A.App
              (A.defaultAppInfo $ getRange (hd, args0, princArg))
              (A.unAppView $ A.Application hd args0)
              princArg
          z <- runExceptT $ checkArgumentsE cmp ExpandLast fun args' tb (snd <$> mt)
          case z of
            Right st@(ACState _ _ trest targetCheck) -> do
              v <- checkHeadConstraints (u `applyE`) st
              return (v, trest, targetCheck)
            Left problem -> do
              -- In the inference case:
              -- To create a postponed type checking problem,
              -- we do not use typeDontCare, but create a meta.
              tc <- caseMaybe mt newTypeMeta_ (return . snd)
              v  <- postponeArgs problem cmp ExpandLast fun args' tb tc \ st@(ACState _ _ trest targetCheck) -> do
                      v <- checkHeadConstraints (u `applyE`) st
                      coerce' cmp targetCheck v trest tc

              return (v, tc, NotCheckedTarget)

-- | Throw 'AmbiguousOverloadedProjection' with additional explanation.
refuseProj :: List1 QName -> TCM Doc -> TCM a
refuseProj ds reason = typeError . AmbiguousOverloadedProjection ds =<< reason

refuseProjNotApplied, refuseProjNoMatching :: List1 QName -> TCM a
refuseProjNotApplied    ds = refuseProj ds $ fwords "it is not applied to a visible argument"
refuseProjNoMatching    ds = refuseProj ds $ fwords "no matching candidate found"
refuseProjNotRecordType :: List1 QName -> Maybe Term -> Type -> TCM a
refuseProjNotRecordType ds pValue pType = do
  let dType = prettyTCM pType
  let dValue = caseMaybe pValue (return empty) prettyTCM
  refuseProj ds $ fsep $
    ["principal argument", dValue, "has type", dType, "while it should be of record type"]

-----------------------------------------------------------------------------
-- * Sorts
-----------------------------------------------------------------------------

checkUniv
  :: UnivSize -> Univ -> Comparison -> A.Expr -> Type
  -> QName -> Suffix -> [NamedArg A.Expr] -> TCM Term
checkUniv sz u cmp e t q suffix args = do
  (v, t0) <- inferUniv sz u e q suffix args
  coerce cmp v t0 t

inferUniv :: UnivSize -> Univ -> A.Expr -> QName -> Suffix -> [NamedArg A.Expr] -> TCM (Term, Type)
inferUniv sz u e q s args = do
  univChecks u
  case sz of
    USmall -> inferLeveledSort u q s args
    ULarge -> inferUnivOmega u q s args

univChecks :: Univ -> TCM ()
univChecks = \case
  UProp -> unlessM isPropEnabled $ typeError NeedOptionProp
  UType -> pure ()
  USSet -> unlessM isTwoLevelEnabled $ typeError NeedOptionTwoLevel

suffixToLevel :: Suffix -> Integer
suffixToLevel = \case
  NoSuffix -> 0
  Suffix n -> n

inferLeveledSort ::
     Univ                -- ^ The universe type.
  -> QName               -- ^ Name of the universe, for error reporting.
  -> Suffix              -- ^ Level of the universe given via suffix (optional).
  -> [NamedArg A.Expr]   -- ^ Level of the universe given via argument (absent if suffix).
  -> TCM (Term, Type)    -- ^ Universe and its sort.
inferLeveledSort u q suffix = \case
  [] -> do
    let n = suffixToLevel suffix
    return (Sort (Univ u $ ClosedLevel n) , sort (Univ (univUniv u) $ ClosedLevel $ n + 1))
  arg : args -> do
    unless (visible arg) $ typeError $ WrongHidingInApplication $ sort $ Univ u $ ClosedLevel 0
    unlessM hasUniversePolymorphism $ typeError NeedOptionUniversePolymorphism
    List1.unlessNull args $ warning . TooManyArgumentsToSort q
    l <- applyRelevanceToContext shapeIrrelevant $ checkLevel arg
    return (Sort $ Univ u l , sort (Univ (univUniv u) $ levelSuc l))

inferUnivOmega ::
     Univ                -- ^ The universe type.
  -> QName               -- ^ Name of the universe, for error reporting.
  -> Suffix              -- ^ Level of the universe given via suffix (optional).
  -> [NamedArg A.Expr]   -- ^ Level of the universe given via argument (should be absent).
  -> TCM (Term, Type)    -- ^ Universe and its sort.
inferUnivOmega u q suffix args = do
    List1.unlessNull args $ warning . TooManyArgumentsToSort q
    let n = suffixToLevel suffix
    return (Sort (Inf u n) , sort (Inf (univUniv u) $ 1 + n))

-----------------------------------------------------------------------------
-- * Coinduction
-----------------------------------------------------------------------------

checkSharpApplication :: A.Expr -> Type -> QName -> [NamedArg A.Expr] -> TCM Term
checkSharpApplication e t c args = do
  arg <- case args of
           [a] | visible a -> return $ namedArg a
           _ -> typeError $ WrongSharpArity c

  -- The name of the fresh function.
  i <- fresh :: TCM Int
  let name = filter (/= '_') (prettyShow $ A.nameConcrete $ A.qnameName c) ++ "-" ++ show i

  kit <- coinductionKit'
  let flat = nameOfFlat kit
      inf  = nameOfInf  kit

  -- Add the type signature of the fresh function to the
  -- signature.
  -- To make sure we can type check the generated function we have to make
  -- sure that its type is \inf. The reason for this is that we don't yet
  -- postpone checking of patterns when we don't know their types (Issue480).
  forcedType <- do
    lvl <- levelType
    (_, l) <- newValueMeta RunMetaOccursCheck CmpLeq lvl
    lv  <- levelView l
    (_, a) <- newValueMeta RunMetaOccursCheck CmpEq (sort $ Type lv)
    return $ El (Type lv) $ Def inf [Apply $ setHiding Hidden $ defaultArg l, Apply $ defaultArg a]

  wrapper <- inFreshModuleIfFreeParams $
             setRunTimeModeUnlessInHardCompileTimeMode $ do
    -- Andreas, 2019-10-12: create helper functions in non-erased mode.
    -- Otherwise, they are not usable in meta-solutions in the term world.
    -- #4743: Except if hard compile-time mode is enabled.
    c' <- setRange (getRange c) <$>
            liftM2 qualify (killRange <$> currentModule)
                           (freshName_ name)

    -- Define and type check the fresh function.
    mod <- currentModality
    abs <- asksTC (^. lensIsAbstract)
    let info   = A.mkDefInfo (A.nameConcrete $ A.qnameName c') noFixity'
                             PublicAccess abs noRange
        core   = A.LHSProj { A.lhsDestructor = unambiguous flat
                           , A.lhsFocus      = defaultNamedArg $ A.LHSHead c' []
                           , A.lhsPats       = [] }
        clause = A.Clause (A.LHS empty core) []
                          (A.RHS arg Nothing)
                          A.noWhereDecls empty

    i <- currentOrFreshMutualBlock

    -- If we are in irrelevant position, add definition irrelevantly.
    -- If we are in erased position, add definition as erased.
    -- TODO: is this sufficient?
    addConstant c' =<< do
      let ai = setModality mod defaultArgInfo
      lang <- getLanguage
      fun  <- emptyFunction
      useTerPragma $
        (defaultDefn ai c' forcedType lang fun)
        { defMutual = i }

    checkFunDef info c' $ singleton clause

    reportSDoc "tc.term.expr.coind" 15 $ do
      def <- theDef <$> getConstInfo c'
      vcat $
        [ "The coinductive wrapper"
        , nest 2 $ prettyTCM mod <> (prettyTCM c' <+> ":")
        , nest 4 $ prettyTCM t
        , nest 2 $ prettyA clause
        ]
    return c'

  -- The application of the fresh function to the relevant
  -- arguments.
  e' <- Def wrapper . map Apply <$> getContextArgs

  reportSDoc "tc.term.expr.coind" 15 $ vcat $
      [ "The coinductive constructor application"
      , nest 2 $ prettyTCM e
      , "was translated into the application"
      , nest 2 $ prettyTCM e'
      ]

  blockTerm t $ e' <$ workOnTypes (leqType forcedType t)

-----------------------------------------------------------------------------
-- * Cubical
-----------------------------------------------------------------------------

-- | "pathAbs (PathView s _ l a x y) t" builds "(\ t) : pv"
--   Preconditions: PathView is PathType, and t[i0] = x, t[i1] = y
pathAbs :: PathView -> Abs Term -> TCM Term
pathAbs (OType _) t = __IMPOSSIBLE__
pathAbs (PathType s path l a x y) t = do
  return $ Lam defaultArgInfo t

-- | @primComp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1@
--
--   Check:  @u i0 = (λ _ → a) : Partial φ (A i0)@.
--
checkPrimComp :: QName -> ArgRanges -> Args -> Type -> TCM Args
checkPrimComp c rs vs _ = do
  case vs of
    -- WAS: [l, a, phi, u, a0] -> do
    l : a : phi : u : a0 : rest -> do
      iz <- Arg defaultArgInfo <$> intervalUnview IZero
      let lz = unArg l `apply` [iz]
          az = unArg a `apply` [iz]
      ty <- el's (pure (unArg l `apply` [iz])) $ primPartial <#> pure (unArg l `apply` [iz]) <@> pure (unArg phi) <@> pure (unArg a `apply` [iz])
      bAz <- el' (pure $ lz) (pure $ az)
      a0 <- blockArg bAz (rs !!! 4) a0 $ do
        equalTerm ty -- (El (getSort t1) (apply (unArg a) [iz]))
          (Lam defaultArgInfo $ NoAbs "_" $ unArg a0)
          (apply (unArg u) [iz])
      return $ l : a : phi : u : a0 : rest
    _ -> typeError $ CubicalPrimitiveNotFullyApplied c

-- | @primHComp : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A@
--
--   Check:  @u i0 = (λ _ → a) : Partial φ A@.
--
checkPrimHComp :: QName -> ArgRanges -> Args -> Type -> TCM Args
checkPrimHComp c rs vs _ = do
  case vs of
    -- WAS: [l, a, phi, u, a0] -> do
    l : a : phi : u : a0 : rest -> do
      -- iz = i0
      iz <- Arg defaultArgInfo <$> intervalUnview IZero
      -- ty = Partial φ A
      ty <- el's (pure (unArg l)) $ primPartial <#> pure (unArg l) <@> pure (unArg phi) <@> pure (unArg a)
      -- (λ _ → a) = u i0 : ty
      bA <- el' (pure $ unArg l) (pure $ unArg a)
      a0 <- blockArg bA (rs !!! 4) a0 $ do
        equalTerm ty -- (El (getSort t1) (apply (unArg a) [iz]))
            (Lam defaultArgInfo $ NoAbs "_" $ unArg a0)
            (apply (unArg u) [iz])
      return $ l : a : phi : u : a0 : rest
    _ -> typeError $ CubicalPrimitiveNotFullyApplied c

-- | @transp : ∀{ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (a0 : A i0) → A i1@
--
--   Check:  If φ, then @A i = A i0 : Set (ℓ i)@ must hold for all @i : I@.
--
checkPrimTrans :: QName -> ArgRanges -> Args -> Type -> TCM Args
checkPrimTrans c rs vs _ = do
  case vs of
    -- Andreas, 2019-03-02, issue #3601, why exactly 4 arguments?
    -- Only 3 are needed to check the side condition.
    -- WAS:
    -- [l, a, phi, a0] -> do
    l : a : phi : rest -> do
      iz <- Arg defaultArgInfo <$> intervalUnview IZero
      -- ty = (i : I) -> Set (l i)
      ty <- runNamesT [] $ do
        l <- open $ unArg l
        nPi' "i" primIntervalType $ \ i -> (sort . tmSort <$> (l <@> i))
      a <- blockArg ty (rs !!! 1) a $ do
        equalTermOnFace (unArg phi) ty
          (unArg a)
          (Lam defaultArgInfo $ NoAbs "_" $ apply (unArg a) [iz])
      return $ l : a : phi : rest
    _ -> typeError $ CubicalPrimitiveNotFullyApplied c

blockArg :: HasRange r => Type -> r -> Arg Term -> TCM () -> TCM (Arg Term)
blockArg t r a m =
  setCurrentRange (getRange $ r) $ fmap (a $>) $ blockTerm t $ m >> return (unArg a)

-- The following comment contains silly ' escapes to calm CPP about ∨ (\vee).
-- May not be haddock-parseable.

-- ' @primPOr : ∀ {ℓ} (φ₁ φ₂ : I) {A : Partial (φ₁ ∨ φ₂) (Set ℓ)}
-- '         → (u : PartialP φ₁ (λ (o : IsOne φ₁) → A (IsOne1 φ₁ φ₂ o)))
-- '         → (v : PartialP φ₂ (λ (o : IsOne φ₂) → A (IsOne2 φ₁ φ₂ o)))
-- '         → PartialP (φ₁ ∨ φ₂) A@
-- '
-- ' Checks: @u = v : PartialP (φ₁ ∨ φ₂) A@ whenever @IsOne (φ₁ ∧ φ₂)@.
checkPOr :: QName -> ArgRanges -> Args -> Type -> TCM Args
checkPOr c rs vs _ = do
  case vs of
   l : phi1 : phi2 : a : u : v : rest -> do
      phi <- intervalUnview (IMin phi1 phi2)
      reportSDoc "tc.term.por" 10 $ text (show phi)
      t1 <- runNamesT [] $ do
             l <- open . unArg $ l
             a <- open . unArg $ a
             psi <- open =<< intervalUnview (IMax phi1 phi2)
             pPi' "o" psi $ \ o -> el' l (a <..> o)
      tv <- runNamesT [] $ do
             l    <- open . unArg $ l
             a    <- open . unArg $ a
             phi1 <- open . unArg $ phi1
             phi2 <- open . unArg $ phi2
             pPi' "o" phi2 $ \ o -> el' l (a <..> (cl primIsOne2 <@> phi1 <@> phi2 <@> o))
      v <- blockArg tv (rs !!! 5) v $ do
        -- ' φ₁ ∧ φ₂  ⊢ u , v : PartialP (φ₁ ∨ φ₂) \ o → a o
        equalTermOnFace phi t1 (unArg u) (unArg v)
      return $ l : phi1 : phi2 : a : u : v : rest
   _ -> typeError $ CubicalPrimitiveNotFullyApplied c

-- | @prim^glue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
--              → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
--              → (t : PartialP φ T) → (a : A) → primGlue A T e@
--
--   Check   @φ ⊢ a = e 1=1 (t 1=1)@  or actually the equivalent:  @(\ _ → a) = (\ o -> e o (t o)) : PartialP φ A@
check_glue :: QName -> ArgRanges -> Args -> Type -> TCM Args
check_glue c rs vs _ = do
  case vs of
   -- WAS: [la, lb, bA, phi, bT, e, t, a] -> do
   la : lb : bA : phi : bT : e : t : a : rest -> do
      v <- runNamesT [] $ do
            lb  <- open . unArg $ lb
            la  <- open . unArg $ la
            bA  <- open . unArg $ bA
            phi <- open . unArg $ phi
            bT  <- open . unArg $ bT
            e   <- open . unArg $ e
            t   <- open . unArg $ t
            let f o = cl primEquivFun <#> lb <#> la <#> (bT <..> o) <#> bA <@> (e <..> o)
            glam defaultIrrelevantArgInfo "o" $ \ o -> f o <@> (t <..> o)
      ty <- runNamesT [] $ do
            lb  <- open . unArg $ lb
            phi <- open . unArg $ phi
            bA  <- open . unArg $ bA
            el's lb $ cl primPartialP <#> lb <@> phi <@> glam defaultIrrelevantArgInfo "o" (\ _ -> bA)
      let a' = Lam defaultIrrelevantArgInfo (NoAbs "o" $ unArg a)
      ta <- el' (pure $ unArg la) (pure $ unArg bA)
      a <- blockArg ta (rs !!! 7) a $ equalTerm ty a' v
      return $ la : lb : bA : phi : bT : e : t : a : rest
   _ -> typeError $ CubicalPrimitiveNotFullyApplied c


-- | @prim^glueU : ∀ {ℓ} {φ : I}
--              → {T : I → Partial φ (Set ℓ)} → {A : Set ℓ [ φ ↦ T i0 ]}
--              → (t : PartialP φ (T i1)) → (a : outS A) → hcomp T (outS A)@
--
--   Check   @φ ⊢ a = transp (\ i -> T 1=1 (~ i)) i0 (t 1=1)@  or actually the equivalent:
--           @(\ _ → a) = (\o -> transp (\ i -> T o (~ i)) i0 (t o)) : PartialP φ (T i0)@
check_glueU :: QName -> ArgRanges -> Args -> Type -> TCM Args
check_glueU c rs vs _ = do
  case vs of
   -- WAS: [la, lb, bA, phi, bT, e, t, a] -> do
   la : phi : bT : bA : t : a : rest -> do
      v <- runNamesT [] $ do
            la  <- open . unArg $ la
            phi <- open . unArg $ phi
            bT  <- open . unArg $ bT
            bA  <- open . unArg $ bA
            t   <- open . unArg $ t
            let f o = cl primTrans <#> lam "i" (const la) <@> lam "i" (\ i -> bT <@> (cl primINeg <@> i) <..> o) <@> cl primIZero
            glam defaultIrrelevantArgInfo "o" $ \ o -> f o <@> (t <..> o)
      ty <- runNamesT [] $ do
            la  <- open . unArg $ la
            phi <- open . unArg $ phi
            bT  <- open . unArg $ bT
            pPi' "o" phi $ \ o -> el' la (bT <@> cl primIZero <..> o)
      let a' = Lam defaultIrrelevantArgInfo (NoAbs "o" $ unArg a)
      ta <- runNamesT [] $ do
            la  <- open . unArg $ la
            phi <- open . unArg $ phi
            bT  <- open . unArg $ bT
            bA  <- open . unArg $ bA
            el' la (cl primSubOut <#> (cl primLevelSuc <@> la) <#> (Sort . tmSort <$> la) <#> phi <#> (bT <@> cl primIZero) <@> bA)
      a <- blockArg ta (rs !!! 5) a $ equalTerm ty a' v
      return $ la : phi : bT : bA : t : a : rest
   _ -> typeError $ CubicalPrimitiveNotFullyApplied c
